﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Epsilon.Expr;

namespace Epsilon.Typing
{
    public class GlobalTypeChecker
    {
        Dictionary<string, TypeChecker> typers = new Dictionary<string, TypeChecker>();
        List<Process> processes;

        public GlobalTypeChecker(List<Process> p)
        {
            processes = p;
        }

        public void TypeCheck()
        {
            for (int i = 0; i < processes.Count; i++)
                typers.Add(processes[i].Name, new TypeChecker(processes[i]));

            foreach (string s in typers.Keys) 
                typers[s].TypeCheck();

            // now check the security constraints, but only to one level
            // for each process
            foreach (string s in typers.Keys)
            {
                // for each tx statement in each process
                foreach (TxExpr tx in typers[s].TxExprs)
                {
                    // if there is a process variable, check against all
                    // processes
                    PidBase pids = (PidBase)tx.Pid.Label.MaxPidLabel;
                    if (pids.Pidvs != null && pids.Pidvs.Count > 0)
                    {
                        foreach (string ss in typers.Keys)
                            if (!CheckConstraint(tx, ss))
                                Error("Transmit statement in process " + s + " at line " +
                                    tx.Line + " col " + tx.Col + " does not satisfy " +
                                        " a receive statement in process " + ss);
                    }
                    else if (pids.Pids != null && pids.Pids.Count > 0)
                    {
                        foreach (PidExpr pe in pids.Pids)
                            if (!CheckConstraint(tx, pe.Pid))
                                Error("Transmit statement in process " + s + " at line " +
                                    tx.Line + " col " + tx.Col + " does not satisfy " +
                                        " a receive statement in process " + pe.Pid);
                    }
                }
            }

            return;
        }

        public void Error(string s)
        {
            throw new TypingException(s);
        }

        // Check the tx statement against all constraints in process proc
        private bool CheckConstraint(TxExpr tx, string proc)
        {
            if (!typers.Keys.Contains(proc))
                return true;

            Type txType = tx.Val.Label.Type;

            foreach (SecConstraint sc in typers[proc].Constraints)
            {
                if (sc.Clause.Type != txType)
                    continue;

                #region calculate security label
                // Security label of the clause and of the message
                SecRLabel clauseSec = typers[proc].RxStore.GetRxSecArg(sc.Clause);
                SecLabel txSec = tx.Label.SecLabel;

                while (clauseSec != null && clauseSec != sc.Label)
                {
                    if (clauseSec is SecVar)
                    {
                        clauseSec = null;
                        break;
                    }
                    else if (clauseSec is SecRTuple)
                    {
                        // Shouldn't need checks here as we know the types are the same
                        SecRTuple ct = (SecRTuple)clauseSec;
                        SecTuple tt = (SecTuple)txSec;
                        bool found = false;
                        for (int i = 0; i < ct.Labels.Count; i++)
                        {
                            if (SecUtil.Vars(ct.Labels[i]).Contains(sc.Label))
                            {
                                found = true;
                                clauseSec = ct.Labels[i];
                                txSec = tt.Labels[i];
                                break;
                            }
                        }
                        if (!found)
                            clauseSec = null;
                    }
                    else if (clauseSec is SecRFun)
                    {
                        Error("Possible security breach - it is not possible verify code" +
                            " that transmits functions between processes");
                    }
                }

                if (clauseSec == null)
                    continue;
                #endregion

                // Now we have the security label in txSec we can check
                Tuple<List<SecVar>, List<ISecPid>> readers = txSec.Readers();

                #region calculate pid label
                if (readers.Item1 == null && readers.Item2 == null)
                    continue;

                if (readers.Item1 != null && readers.Item1.Count > 0)
                    return false;

                if (readers.Item2 != null && readers.Item2.Count == 0)
                    return false;

                // CHECK IF THE PID LABEL IS A SINGLE PID
                if (sc.Process is PidExpr)
                {
                    if (readers.Item2.IndexOf((PidExpr)(sc.Process)) < 0)
                        return false;
                    else
                        continue;
                }

                // now the set of readers has been calculated,
                // calculate the set of process id's
                PidRLabel clausePid = typers[proc].RxStore.GetRxPidMaxArg(sc.Clause);
                PidLabel txPid = tx.Val.Label.MaxPidLabel;

                while (clausePid != null && clausePid != (PidVar)(sc.Process))
                {
                    if (clausePid is PidVar)
                    {
                        clausePid = null;
                        break;
                    }
                    else if (clausePid is PidRTuple)
                    {
                        // Shouldn't need checks here as we know the types are the same
                        PidRTuple ct = (PidRTuple)clausePid;
                        PidTuple tt = (PidTuple)txPid;
                        bool found = false;
                        for (int i = 0; i < ct.Labels.Count; i++)
                        {
                            if (PidUtil.Vars(ct.Labels[i]).Contains((PidVar)(sc.Process)))
                            {
                                found = true;
                                clausePid = ct.Labels[i];
                                txPid = tt.Labels[i];
                                break;
                            }
                        }
                        if (!found)
                            clausePid = null;
                    }
                    else if (clausePid is PidRFun)
                    {
                        Error("Possible security breach - it is not possible verify code" +
                            " that transmits functions between processes");
                    }
                }

                if (clausePid == null)
                    continue;

                #endregion

                PidBase pb = txPid as PidBase;
                if (pb == null)
                    Error("Process id expression does not have a base label");

                // now check if all the process id's and vars are in the label
                if (pb.Pids != null)
                {
                    foreach (PidExpr p in pb.Pids)
                    {
                        if (readers.Item2.IndexOf(p) < 0)
                            return false;
                    }
                }
                if (pb.Pidvs != null)
                {
                    foreach (PidVar v in pb.Pidvs)
                    {
                        if (readers.Item2.IndexOf(v) < 0)
                            return false;
                    }
                }
            }

            return true;
        }
    }
}
